package verificateur;
import instruction.Affectation;

import java.io.IOException;
import java.util.LinkedList;

import structureDonnee.Block;
import structureDonnee.Expression;
import structureDonnee.Inequalite;
import structureDonnee.Invariant;
import structureDonnee.Node;

import math.Fraction;

public class Verificateur0 {
	
	public Verificateur0(){}
	
	//alogrithm fourrier Motzkin pour Post Condition apres une affectation
	public Invariant postCondition(Invariant inv, 
									Affectation aff, 
									EnsembleVariable ev){
		int n = ev.size();
//		int index = ev.listeVariable.indexOf(aff.v);
		//chercher le nom de variable de v
		int index=0;
		while(!aff.getVariable().getNom().equals(ev.getListeVariable().get(index).getNom())){
			index++;
			if(index==n) System.out.println("AffectationToVariableUnknown");
		}		
		LinkedList<Inequalite> listIneNew = new LinkedList<Inequalite>();

		double aj=aff.getExpr().getListExpr().get(index);
		//aj cas de inversible
		if(aj!=0){
			//pour chaque ine
			for(Inequalite ine : inv.getListIne()){
				LinkedList<Double> listtmp = new LinkedList<Double>();

				for (int i = 0; i < n; i++){
					if(i!=index){
						//calcule nouveau a(i) i!=j
						double aai = ine.getExpr().getListExpr().get(i)-ine.getExpr().getListExpr().get(index)/aj*aff.getExpr().getListExpr().get(i);
						listtmp.add(i, aai);
					}
					else{
						//calcule nouveua a(j)
						double aaj = ine.getExpr().getListExpr().get(index)/aj;
						listtmp.add(index, aaj);
					}
				}
				//calculte constant
				double dd = ine.getExpr().getListExpr().get(n)-ine.getExpr().getListExpr().get(index)/aj;//constant
				listtmp.add(n, dd);

				Inequalite ineNew = new Inequalite(new Expression(listtmp));
				listIneNew.add(ineNew);
			}
			return new Invariant(listIneNew);
		}

		//aj cas de non-inversible
		else{
			LinkedList<Inequalite> listIneNewPos = new LinkedList<Inequalite>();
			LinkedList<Inequalite> listIneNewNeg = new LinkedList<Inequalite>();
			
			for(Inequalite ine : inv.getListIne()){
				double ajj=ine.getExpr().getListExpr().get(index);
				//inequelite de type III
				if(ajj==0){
					 listIneNew.add(ine);
				}
				else{
					//inequalite de type I
					if (ajj>0){
						LinkedList<Double> dl= new LinkedList<Double>();
						//ajouter des coeffi
						for(int i = 0; i<n ; i++){
							if(i!=index){
								dl.add(i, (-1)*ine.getExpr().getListExpr().get(i)/ajj);
							}
							else{
								dl.add(index,0.0);
							}
						}
						//ajouter constant
						dl.add(n, (-1)*ine.getExpr().getListExpr().get(n)/ajj);
						listIneNewPos.add(new Inequalite(new Expression(dl)));
					}
					//inequelite de type II
					if (ajj<0){
						LinkedList<Double> dl= new LinkedList<Double>();
						//ajouter des coeffi
						for(int i = 0; i<n ; i++){
							if(i!=index){
								dl.add(i, (-1)*ine.getExpr().getListExpr().get(i)/ajj);
							}
							else{
								dl.add(index,0.0);
							}
						}
						//ajouter constant
						dl.add(n, (-1)*ine.getExpr().getListExpr().get(n)/ajj);
						listIneNewNeg.add(new Inequalite(new Expression(dl)));
					}
				} 
			}
			
			for (Inequalite inePos:listIneNewPos){
				for (Inequalite ineNeg:listIneNewNeg){
					LinkedList<Double> dll = new LinkedList<Double>();
					for(int i = 0; i< n+1; i++){
						double tmp = ineNeg.getExpr().getListExpr().get(i)-inePos.getExpr().getListExpr().get(i);
						dll.add(i, tmp);
					}
					Inequalite ineNew = new Inequalite(new Expression(dll));
					listIneNew.add(ineNew);
				}
			}
			return new Invariant(listIneNew);
		}
	}
	
	//verifier un node, un Invariant. Inv.mEnviron => Inv.invariant
	public boolean verifierNode(Node node, EnsembleVariable ev){
		//on utilise class simplex pour verifier implication.
		Simplex sim = new Simplex();
		boolean YesNo = sim.verifierImplication(node.getEnviron(), node.getInvariant());
System.out.println("verifierNODE");		

		if(node.getInstr().getType() == 0 ){ //instruction is affectation, executer aff
			if(!node.getSuivants().isEmpty()){
	//			executerAffectation(node,ev);
				Invariant tmpInv = postCondition(node.getInvariant(),node.getInstr(),ev);
				node.suivants.getFirst().environ = new Invariant();
				node.suivants.getFirst().environ.listIne.addAll(tmpInv.listIne);
System.out.println("executerAffecatation");	
			}
			else System.out.println("Wrong!NodeFinDeArbreAvecAffectation");
		}
		if(node.instr.getType() == 1){//instruction FaireRien
			if(node.suivants == null){
System.out.println("fin de arbre");
			}
			else{
				if(!node.suivants.isEmpty()){}
				else
System.out.println("fin de arbre");
			}
		}
		if(node.instr.getType() == 2){//update
			if(!node.suivants.isEmpty()){ //instruction is update instruction
				Invariant tmpInv = node.getInstr().update;
				node.suivants.getFirst().environ = new Invariant();
				node.suivants.getFirst().environ.listIne.addAll(tmpInv.listIne);
			}
			else
System.out.println("fin de arbre");
		}
		return YesNo;
	}
	
	// executer affectation en utilisant post condition;mettre a jour aff.destination.environment
	public void executerAffectation(Node node, EnsembleVariable ev){
		Invariant tmpInv = postCondition(node.invariant,node.instr,ev);
		node.suivants.getFirst().environ = tmpInv;
System.out.println("executerAffecatation");		
	}
	
	// verifier un arbre, un program en effet. en recurrence.
	public boolean verifierArbre(Node node, EnsembleVariable ev){
		boolean OuiNon = true;
		LinkedList<Node> visited = new LinkedList<Node>();
		visited.add(node);
		OuiNon = OuiNon & verifierNode(node,ev);
		if(node.suivants!=null){
			for(Node nodetmp : node.suivants){
	//			executerAffectation(nodetmp,ev);
				if(!visited.contains(nodetmp)){
					visited.add(nodetmp);
					OuiNon = OuiNon&verifierArbre(nodetmp,ev);
				}
			}
		}
System.out.println("verifierArbre");		
		return OuiNon;
	}
	

	
	
	public static void main(String[] args) throws IOException {
		
		//pour l instant, on suppose qu' il n'y a pas de "space"(ascii=32) in .txt.
//	    String nomDeFichier = "W3.txt";	
	    
	    //construct ensemble variable
//		EnsembleVariable ens = new EnsembleVariable(nomDeFichier);
		EnsembleVariable ens = new EnsembleVariable("tmp.txt");
		System.out.print(ens.size() + " VARIABLES: ");for (int i = 0; i < ens.size(); i++) System.out.print(ens.getVariable(i).getNom()+",");System.out.println();
	
///////////////////////////////////////////////////////////////////////////////    	
       	//pour tester constructor des Class
//	    Expression ex = new Expression("+1+23*i-4*j0+6000*k",ens);ex.publish(ens);System.out.println();
	    	
//	    Inequalite ine = new Inequalite("+1+23*i-4*j0+6000*k<=0",ens);ine.pulish(ens);System.out.println();
//	    ine.not().pulish(ens);System.out.println();
//	    Invariant inv = new Invariant("{+0+1*i+1*j0+1*k>=0,+0+1*i+2*j0+3*k<=0}",ens);inv.publish(ens);
//	    Affectation aff = new Affectation("[i=+1+23*i-4*j0+6000*k]",ens);aff.publish(ens);System.out.println();
       	
//////////////////////////////////////////////////////////	
	   	String testStr1 = "{+1+1*i+1*j0+1*k>=0}\n" +
	    			"[i=+2+2*i-4*j0+1*k]\n" +
	    			"{+3+5*i-4*j0+3*k>=0}\n" +
	    			"[i=+4+3*i-4*j0+2*k]\n" +
	    			"{+5+2*i-1*j0+5*k>=0}\n" +
//	    			"[i=+700+3*i-4*j0+2*k]\n" +
//	    			"{+800+2*i-1*j0+5*k>=0}\n" +
	    			"@";


    	String testStr2 = 
//			"{-1+3*i+1*j>=0}\n" +
//			"[j=+0+2*i+3*j]\n" +
    		"{+1+0*i+0*j>=0}\n" +
    		"if(+2+1*i+0*j>=0){\n" +
    			"{+3+1*i+0*j>=0}\n" +
    		"@}\n" +
    		"else{\n" +
    			"{+4+1*i+0*j>=0}\n" +
    		"@}\n" +
    		"{+5+0*i+1*j>=0}\n" +
//			"[j=+6+2*i+3*j]\n" +
//			"{+7+3*i+1*j>=0}\n" +
//			"[j=+8+2*i+3*j]\n" +
//			"{+9+3*i+1*j>=0}\n" +
    		"@";
    	String testStr3 = 
    		"{+1+1*i+2*j>=0}\n" +
    		"if(+2+1*i+3*j>=0){\n" +
    			"{+3+1*i+5*j>=0}\n" +
    			"[j=+4+2*i+3*j]\n" +
    			"{+5+3*i+1*j>=0}\n" +
    		"@}\n" +
    		"else{\n" +
    			"{+6+1*i+7*j>=0}\n" +
    			"[j=+7-1*i+2*j]\n" +
    			"{+8-1*i+9*j>=0}\n" +
    		"@}\n" +
    		"{+9+4*i+1*j>=0}\n" +
    		"@";

    	String testStr4 = 
    	"{+1+1*i+2*j>=0}\n" +
		"if(+2+1*i+3*j>=0){\n" +
			"{+3+1*i+5*j>=0}\n" +
			"[j=+4+2*i+3*j]\n" +
			"{+5+3*i+1*j>=0}\n" +
			"[j=+6-1*i+2*j]\n" +
			"{+7+1*i+7*j>=0}\n"+
		"@}\n" +
		"else{\n" +
			"{+8-1*i+9*j>=0}\n" +
		"@}\n" +
		"{+9+4*i+1*j>=0}\n" +
		"@";
    	String testStr5 = 
        	"{+1+1*i+2*j>=0}\n" +
			"[j=+2+2*i+3*j]\n" +
			"{+3+3*i+1*j>=0}\n" +
    		"if(+4+1*i+3*j>=0){\n" +
    			"{+5+1*i+5*j>=0}\n" +
    			"[j=+6-1*i+2*j]\n" +
    			"{+7+1*i+7*j>=0}\n"+
    		"@}\n" +
    		"else{\n" +
    			"{+8-1*i+9*j>=0}\n" +
    		"@}\n" +
    		"{+9+4*i+1*j>=0}\n" +
    		"@";
    	
    	String testStr6 = 
    	"{+1+0*i+0*j>=0}\n" +
		"if(+2+0*i+0*j>=0){\n" +
			"{+3+0*i+0*j>=0}\n" +
			"if(+4+1*i+0*j>=0){\n" +
				"{+5+1*i+0*j>=0}\n" +
			"@}\n" +
			"else{\n" +
				"{+6+1*i+0*j>=0}\n" +
			"@}\n" +
			"{+7+0*i+1*j>=0}\n" +
		"@}\n" +
		"else{\n" +
			"{+8+0*i+0*j>=0}\n" +
		"@}\n" +
		"{+9+0*i+0*j>=0}\n"+
		"@";
    	String testStr7 = 
			"{-1+3*i+1*j>=0}\n" +
			"[j=+0+2*i+3*j]\n" +
        	"{+1+0*i+0*j>=0}\n" +
    		"if(+2+0*i+0*j>=0){\n" +
    			"{+3+0*i+0*j>=0}\n" +
    			"if(+4+1*i+0*j>=0){\n" +
    				"{+5+1*i+0*j>=0}\n" +
    			"@}\n" +
    			"else{\n" +
    				"{+6+1*i+0*j>=0}\n" +
    			"@}\n" +
    			"{+7+0*i+1*j>=0}\n" +
    		"@}\n" +
    		"else{\n" +
				"{+8+0*i+0*j>=0}\n" +
				"if(+9+1*i+0*j>=0){\n" +
					"{+10+1*i+0*j>=0}\n" +
					"[j=+11-1*i+2*j]\n" +
					"{+12+1*i+7*j>=0}\n"+
				"@}\n" +
				"else{\n" +
					"{+13+1*i+0*j>=0}\n" +
				"@}\n" +
				"{+14+0*i+1*j>=0}\n" +
				"[j=+15-1*i+2*j]\n" +
				"{+16+1*i+7*j>=0}\n"+
			"@}\n" +
			"{+17+1*i+5*j>=0}\n" +
			"[j=+18-1*i+2*j]\n" +
			"{+19+1*i+7*j>=0}\n"+
    		"@";
    	String testStr8 = 
        	"{+1+0*i+0*j>=0}\n" +
    		"if(+2+0*i+0*j>=0){\n" +
    			"{+3+0*i+0*j>=0}\n" +
    			"if(+4+1*i+0*j>=0){\n" +
    				"{+5+1*i+0*j>=0}\n" +
    			"@}\n" +
    			"else{\n" +
	    			"{+6+0*i+0*j>=0}\n" +
	    			"if(+7+1*i+0*j>=0){\n" +
	    				"{+8+1*i+0*j>=0}\n" +
	    			"@}\n" +
	    			"else{\n" +
	    				"{+9+1*i+0*j>=0}\n" +
	    			"@}\n" +
	    			"{+10+0*i+1*j>=0}\n" +
    			"@}\n" +
    			"{+11+0*i+1*j>=0}\n" +
    		"@}\n" +
    		"else{\n" +
    			"{+12+0*i+0*j>=0}\n" +
    		"@}\n" +
    		"{+13+0*i+0*j>=0}\n"+
    		"@";
    	String testStr9 = 
        	"{+1+0*i+0*j>=0}\n" +
    		"if(+2+0*i+0*j>=0){\n" +
    			"{+3+0*i+0*j>=0}\n" +
    			"if(+4+1*i+0*j>=0){\n" +
	    			"{+5+0*i+0*j>=0}\n" +
	    			"if(+6+1*i+0*j>=0){\n" +
	    				"{+7+1*i+0*j>=0}\n" +
	    			"@}\n" +
	    			"else{\n" +
	    				"{+8+1*i+0*j>=0}\n" +
	    			"@}\n" +
	    			"{+9+0*i+1*j>=0}\n" +
    			"@}\n" +
    			"else{\n" +
					"{+10+1*i+0*j>=0}\n" +
    			"@}\n" +
    			"{+11+0*i+1*j>=0}\n" +
    		"@}\n" +
    		"else{\n" +
    			"{+12+0*i+0*j>=0}\n" +
    		"@}\n" +
    		"{+13+0*i+0*j>=0}\n"+
    		"@";
    	String testStr10 = 
        	"{+1+0*i+0*j>=0}\n" +
    		"if(+2+0*i+0*j>=0){\n" +
    			"{+3+0*i+0*j>=0}\n" +
    			"if(+4+1*i+0*j>=0){\n" +
	    			"{+5+0*i+0*j>=0}\n" +
	    			"if(+6+1*i+0*j>=0){\n" +
	    				"{+7+1*i+0*j>=0}\n" +
		    			"if(+8+1*i+0*j>=0){\n" +
		    				"{+9+1*i+0*j>=0}\n" +
	    				"@}\n" +
	    				"else{\n" +
	    					"{+10+1*i+0*j>=0}\n" +
	    				"@}\n" +
	    				"{+11+1*i+0*j>=0}\n" +	
	    			"@}\n" +
	    			"else{\n" +
	    				"{+12+1*i+0*j>=0}\n" +
	    			"@}\n" +
	    			"{+13+0*i+1*j>=0}\n" +
    			"@}\n" +
    			"else{\n" +
					"{+14+1*i+0*j>=0}\n" +
    			"@}\n" +
    			"{+15+0*i+1*j>=0}\n" +
    		"@}\n" +
    		"else{\n" +
    			"{+16+0*i+0*j>=0}\n" +
    		"@}\n" +
    		"{+17+0*i+0*j>=0}\n"+
    		"@";
    	
    	String testStrW1 = //{}while(){{}}{}
//			"{-1+3*i+1*j>=0}\n" +
//			"[j=+0+2*i+3*j]\n" +
    		"{+1+0*i+0*j>=0}\n" +
    		"while(+2+1*i+0*j>=0){\n" +
    			"{+3+1*i+0*j>=0}\n" +
 //   			"[j=+33+2*i+3*j]\n" +
 //       		"{+333+1*i+0*j>=0}\n" +
    		"@}\n" +
    		"{+4+0*i+1*j>=0}\n" +
			"[j=+5+2*i+3*j]\n" +
			"{+6+3*i+1*j>=0}\n" +
//			"[j=+7+2*i+3*j]\n" +
//			"{+8+3*i+1*j>=0}\n" +
    		"@";
    	
    	String testStrW2 =  // while(){if(){}else{}}
//			"{-1+3*i+1*j>=0}\n" +
//			"[j=+0+2*i+3*j]\n" +
    		"{+1+0*i+0*j>=0}\n" +
    		"while(+2+1*i+0*j>=0){\n" +
	    		"{+3+1*i+0*j>=0}\n" +
				"if(+4+1*i+0*j>=0){\n" +
					"{+5+1*i+0*j>=0}\n" +
				"@}\n" +
				"else{\n" +
					"{+6+1*i+0*j>=0}\n" +
				"@}\n" +
				"{+7+1*i+0*j>=0}\n" +	
    		"@}\n" +
    		"{+8+0*i+1*j>=0}\n" +
    		"@";
 
    	String testStrW3 =  // if(){ while(){} }else{}
    		"{+1+0*i+0*j>=0}\n" +
			"if(+2+1*i+0*j>=0){\n" +
    			"{+3+1*i+0*j>=0}\n" +
    			"while(+4+1*i+0*j>=0){\n" +
	    			"{+5+1*i+0*j>=0}\n" +
				"@}\n" +
				"{+6+1*i+0*j>=0}\n" +	
    		"@}\n" +
			"else{\n" +
				"{+7+1*i+0*j>=0}\n" +
			"@}\n" +
    		"{+8+0*i+1*j>=0}\n" +
    		"@";
    
    	String testStrW4 =  //  while(){while(){}} 
    		"{+1+0*i+0*j>=0}\n" +
			"while(+2+1*i+0*j>=0){\n" +
    			"{+3+1*i+0*j>=0}\n" +
    			"while(+4+1*i+0*j>=0){\n" +
    			"{+5+1*i+0*j>=0}\n" +
    			"@}\n" +
				"{+6+1*i+0*j>=0}\n" +
			"@}\n" +
			"{+7+1*i+0*j>=0}\n" +	
    		"@";

	    Block blc = new Block(testStr2,ens);blc.publish(blc.getmFirstNode(), ens);
//	    Block blc = new Block(nomDeFichier);blc.publish(blc.getmFirstNode(),ens);
	    Verificateur0 v0 = new Verificateur0();	System.out.println("VOTRE PROGRAMME EST:"+v0.verifierArbre(blc.getmFirstNode(), ens));System.out.println();blc.publish(blc.getmFirstNode(), ens);System.out.println();

	    /*	pour tester fonction post-condition
	    	Verificateur0 verif = new Verificateur0();
	    	Invariant inv0 = new Invariant();
	    	Invariant invv = new Invariant("{+1+1*i+1*j0+1*k>=0,+0+1*i+2*j0+1*k<=0,+0+1*i+0*j0+1*k>=0}",ens);//tester typeIII:typeI=1,typeII=1,typeIII=1
//	    	Invariant invv = new Invariant("{+1+1*i+1*j0+1*k>=0,+0+1*i+2*j0+1*k<=0}",ens);//tester typeI=1,typeII=1,typeIII=0
//	    	Invariant invv = new Invariant("{+1+1*i+1*j0+1*k>=0,+0+1*i+2*j0+1*k>=0,+0+1*i+0*j0+1*k>=0}",ens);//tester typeI=2,typeII=0
	    	Affectation afff = new Affectation("[j0=+1+0*i+2*j0+0*k]",ens);//affectation inversible
//	    	Affectation afff = new Affectation("[j0=+1+0*i+0*j0+0*k]",ens);//affectation non-inversible
	    	inv0 = verif.postCondition(invv, afff, ens);
	    	inv0.publish(ens);
	     */
	}
}
